Thanks — the Exercise 11.5.1 catch here was a real one, and I've landed it separately in #620 with credit to you. ContinuousOn (fun x ↦ 1/x) (Icc 0 1) was genuinely false, so that sorry was unprovable.

I'm closing this PR rather than merging it, because the rest of the changes are docstring disambiguation, and that premise doesn't hold for this repo. Repeated identical exercise docstrings are intentional house style — 12x /-- Exercise 5.4.9 -/, 6x /-- Exercise 3.5.4 -/, and so on — and there's no label or anchor machinery keyed on docstring text (literate.toml sets docstrings_as_text = true, so anchors come from declaration names). That's also why CI was green: there was nothing being fixed. This PR had also gone out of date, with conflicts in Sections 11.3 and 11.5.

If you'd like to propose changing the convention, please open an issue so it can be settled repo-wide.

Statement corrections like the 11.5.1 one — false or mis-hypothesized sorryd goals, in the spirit of #517 — remain very welcome, and are best sent on their own rather than bundled with cosmetic edits.

Reopening — please disregard my previous comment, which was wrong.

I assessed this against a stale checkout of main that was roughly 200 commits behind origin/main. The duplicate-docstring counts I cited (12x /-- Exercise 5.4.9 -/ and so on) were from that stale tree; those had already been fixed on main by #616 and the other label PRs. The label-disambiguation work is an active and accepted cleanup here, not a departure from house style, and this PR is a legitimate continuation of it.

Apologies for the noise.

Could you rebase this on current main? It has conflicts in Sections 11.3 and 11.5.

Note that part of it has since landed independently: #613 (commit be2e4de) already made Exercise 11.5.1 ¬ ContinuousOn and split the Ex. 11.3.1 labels, so those hunks can be dropped. What's still wanted here is the Exercise 11.6.4 (a)/(b) split and the Exercise 3.1.7–3.1.9 part labels.

rebased onto main; dropped the 11.3.1 and 11.5.1 hunks (already in via #613) and kept the 11.6.4 (a)/(b) split plus the 3.1.7–3.1.9 part labels.